\begin{tabbing}
es{-}bc\=\{i:l\}\+
\\[0ex](${\it es}$; $e$; ${\it e'}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=Case TERMOF\{decidable\_\_es{-}causl:ObjectId, 1:l, i:l\}(${\it es}$,${\it e'}$,$e$) of\+
\\[0ex]inl($x$) $\Rightarrow$ true$_{2}$
\\[0ex]inr($x$) $\Rightarrow$ false$_{2}$
\-
\end{tabbing}